This PR replaces the line-based coverage instrumentation we introduced in #2609 with the standard source-based code coverage instrumentation performed by the Rust compiler.

As a result, we now insert code coverage checks in the StatementKind::Coverage(..) statements produced by the Rust compiler during compilation. These checks include coverage-relevant information¹ such as the coverage counter/expression they represent ². Both the coverage metadata (kanimap) and coverage results (kaniraw) are saved into files after the verification stage.

Unfortunately, we currently have a chicken-egg problem with this PR and #3121, where we introduce a tool named kani-cov to postprocess coverage results. As explained in #3143, kani-cov is expected to be an alias for the cov subcommand and provide most of the postprocessing features for coverage-related purposes. But, the tool will likely be introduced after this change. Therefore, we propose to temporarily print a list of the regions in each function with their associated coverage status (i.e., COVERED or UNCOVERED).

Source-based code coverage: An example

The main advantage of source-based coverage results is their precision with respect to the source code. The Source-based Code Coverage documentation explains more details about the LLVM coverage workflow and its different options.

For example, let's take this Rust code:

1 fn _other_function() {
2    println!("Hello, world!");
3 }
4
5 fn test_cov(val: u32) -> bool {
6     if val < 3 || val == 42 {
7         true
8     } else {
9         false
10    }
11 }
12
13 #[cfg_attr(kani, kani::proof)]
14 fn main() {
15    let test1 = test_cov(1);
16    let test2 = test_cov(2);
17    assert!(test1);
18    assert!(test2);
19 }

Compiling and running the program with rustc and the -C instrument-coverage flag, and using the LLVM tools can get us the following coverage result:

In contrast, the cargo kani --coverage -Zsource-coverage command currently generates:

src/main.rs (main)
 * 14:1 - 19:2 COVERED

src/main.rs (test_cov)
 * 5:1 - 6:15 COVERED
 * 6:19 - 6:28 UNCOVERED
 * 7:9 - 7:13 COVERED
 * 9:9 - 9:14 UNCOVERED
 * 11:1 - 11:2 COVERED

which is a verification-based coverage result almost equivalent to the runtime coverage results.

Benchmarking

We have evaluated the performance impact of the instrumentation using the kani-perf.sh suite (14 benchmarks). For each test, we compare the average time to run standard verification against the average time to run verification with the source-based code coverage feature enabled³.

The evaluation has been performed on an EC2 m5a.4xlarge instance running Ubuntu 22.04. The experimental data has been obtained by running the kani-perf.sh script 10 times for each version (only verification and verification + coverage), computing the average and standard deviation. We've split this data into small (tests taking 60s or less) and large (tests taking more than 60s) and drawn the two graphs below.

Performance comparison - small benchmarks

Performance comparison - large benchmarks

Comments on performance

Looking at the small tests, the performance impact seems negligible in such cases. The difference is more noticeable in the large tests, where the time to run verification and coverage can take 2x or even more. It wouldn't be surprising that, as programs become larger, the complexity of the coverage checking grows exponentially as well. However, since most verification jobs don't take longer than 30min (1800s), it's OK to say that coverage checking represents a 100-200% slowdown in the worst case w.r.t. standard verification.

It's also worth noting a few other things:

• The standard deviation remains similar in most cases, meaning that the coverage feature doesn't have an impact on their stability.
• We haven't tried any SAT solvers other than the ones used by default for each benchmark. It's possible that other solvers perform better/worse with the coverage feature enabled.

Call-outs

• The soundness issue documented in Rust's coverage instrumentation assumes function calls never panic #3441.
• The issue with saving coverage mappings for non-reachable functions documented in Coverage metadata should include mappings for all source code #3445.
• I've modified the test cases in tests/coverage/ to test this feature. Since this technique is simpler, we don't need that many test cases. However, it's possible I've left some test cases which don't contribute much. Please let me know if you want to add/remove a test case.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.